% =====================================================================
% HOL Manual LaTeX Source: reference manual
% =====================================================================

\documentclass[12pt,fleqn]{book}
%\usepackage{amsmath}
\usepackage{alltt}
\usepackage{../LaTeX/layout}
\usepackage{imakeidx}
\usepackage{alltt}
\usepackage{fancyvrb}
\usepackage{graphicx}

% ---------------------------------------------------------------------
% Read in defined macros and commands
% ---------------------------------------------------------------------
\input{../LaTeX/commands}
\input{../LaTeX/ref-macros}

\usepackage[hidelinks,hypertexnames=false,pdftitle={The HOL System REFERENCE}]{hyperref}
\usepackage{breakurl} % it depends on hyperref

%\includeonly{title,contents,preface,tactics,index}

\verbosereftrue                           % verbose typesetting
%\includeonly{theorems}
%\includeonly{rules}

\indexsetup{level=\chapter}
\makeindex

\begin{document}

   \emergencystretch=14pt

   \setlength{\unitlength}{1mm}           % unit of length = 1mm
   \setlength{\baselineskip}{16pt}        % line spacing = 16pt

   % ---------------------------------------------------------------------
   % prelims
   % ---------------------------------------------------------------------

%   \pagenumbering{roman}                  % roman page numbers for prelims
%   \setcounter{page}{1}                   % start at page 1

   \include{title}                        % reference title page
   \include{preface}                      % preface to reference manual
   \input{../LaTeX/ack}                   % global acknowledgements
   \tableofcontents                       % table of contents

   % ---------------------------------------------------------------------
   %
   % ---------------------------------------------------------------------

%   \cleardoublepage
%   \pagenumbering{arabic}                % arabic page numbers
%   \setcounter{page}{1}                  % start at page 1

   \include{entries-intro}
   \include{entries}                     % manual entries
   % \include{theorems}                    % pre-proved theorems

   {\def\#{\char'043}                    % \tt style `#' character
    \cleardoublepage
    \printindex
  }

\end{document}
